Definitions | Type, x.A(x),  x. t(x), #$n, A B, n-m, -n, n+m, a<b, Void, x:A B(x), P  Q, False, , S T, inl(x),  b, , s = t, Prop, P & Q, P  Q, false , i= j, , inr(x), World, E, i j, <a,b>, w-pred(w;e), Unit, 2of(t), 1of(t), a(i;t), isnull(a), b, A, , Id, x:A B(x), {x:A| B(x) }, left+right, t T, x:A. B(x) |